Abstract

We are designing a software development paradigm to increase the quality of the resulting software systems while keeping production costs down.  The paradigm relies heavily on the application of automated reasoning techniques in several states of the software development process, in particular, during design and testing.  The paradigm leads to software systems of higher quality through formal verification of specifications in the design states.  Assuring specification correctness at such an early stage in the development process means that fewer major errors propagate through the coding state to be discovered during testing, which in turn decreases the time needed to correct them.  Our software development paradigm provides for reusing verification models in the testing stage to derive test cases, correct behavior in response to the test cases, and the test drivers for coded modules.

We are currently building a system to implement the paradigm, focusing on telecommunication software systems that are specified in a formal description language.  As a base case, we selected SDL, an accepted, stable and widely used formal language.  Our major tool in this effort is system ACL2, which provides the necessary capabilities for theorem proving and execution within a unified environment of a subset of Common Lisp.  Presently, the project is concerned with providing a theorem proving tool for the SDL specifications.

Students

• Olga Shumsky Matlin

Publications

1. O. Shumsky and L. Henschen, "Developing a Framework for Simulation, Verification and Testing of SDL Specification," Proc. of the ACL Workshop, Austin, TX, October 2000.